Inference at * 1 1 
Iof proof for Lemma fseg extend:



1. T : Type
2. l1 : T List
3. v : T
4. l2 : T List
5. L : T List
6. l2 = (L @ l1)
7. ||l1|| < ||l2||
8. l2[(||l2|| - (||l1||+1))] = v
9. (null(L))
10. L' : T List
11. L = (L' @ [last(L)])
  (L' @ [last(L)] @ l1) = (L' @ [v / l1]) 

latex

 by ((((((EqCD) 
CollapseTHEN (Auto))) 
CollapseTHEN (Reduce 0))) 
CollapseTHEN (((EqCD) 

CoCollapseTHEN (Auto)))) 

latex

C1: .....subterm..... T:t1:n

C1:   last(L) = v
C.

Definitions	x:A. B(x), x:AB(x), , T, True, t  T, A List, [car / cdr], [], l[i], n - m, n+m, #$n, last(L), as @ bs, A, a < b, type List, Type, s = t, ||as||
Lemmas	append wf, squash wf, true wf